package ch.epfl.lara.pm.formdecider;

import ch.epfl.lara.pm.ast._

object FormDeciderFormulaStringer {
  
  def apply(expr: Expr) = asString(expr)
  
  def apply(formula: Formula) = asString(formula)
  
  private def asString(expr: Expr): String = expr match {
    case Var(name) => name
    
    case Number(n) => n+""  
      
    case IsInstanceOf(e,tpe) => asString(e) + " : " + tpe
  
    case Plus(left,right) => "(" + asString(left) + "+" + asString(right) + ")" 
    
    case Minus(left,right) => "(" + asString(left) + "-" + asString(right) + ")"
    
    case Prod(left,right) => "(" + asString(left) + "*" + asString(right) + ")" 
    
    case Div(left,right) => "(" + asString(left) + "/" + asString(right) + ")"
    
    case Mod(left,right) => "(" + asString(left) + "%" + asString(right) + ")"
    
    case Eq(left,right) => "(" + asString(left) + "=" + asString(right) + ")"
    
    case Less(left,right) => "(" + asString(left) + "<" + asString(right) + ")"
    
    case LessEq(left,right) => "(" + asString(left) + "<=" + asString(right) + ")"
    
    case EAnd(left,right) => "(" + asString(left) + ") & (" + asString(right) + ")"
    
    case EOr(left,right) => "(" + asString(left) + ") | (" + asString(right) + ")"
    
    case EImply(left,right) => "(" + asString(left) + ") --> (" + asString(right) + ")"

    case Not(e) => "~(" + asString(e) + ")" 

    case NotEq(left,right)  => asString(Not(Eq(left,right)))
    
    case True => "true"
      
    case False => "false"
      
    case _ => error(this+"does not accept expr "+expr)
  }
  
  private def asString(formula: Formula): String = formula match {
    case And(left,right) => "(" + asString(left) + ") & (" + asString(right) + ")"
      
    case Or(left,right) => "(" + asString(left) + ") | (" + asString(right) + ")"
      
    case Imply(left,right) => "(" + asString(left) + ") --> (" + asString(right) + ")"
      
    case Neg(f) => "~(" + asString(f) + ")"
      
    case SubsetEq(left,right) => "(" + asString(left) + ")" + " \\<subseteq> " + "(" + asString(right) + ")"
      
    case In(x,set) =>  x + " : " + asString(set)
    
    case Union(left,right) => asString(left) + " Un " + asString(right)
    
    case Intersection(left,right) => asString(left) + " Int " + asString(right)
    
    case Set(name) => name
    
    case EmptySet => "{}"
      
    case BTrue => "true"
      
    case BFalse => "false"
  }
 
  
  override def toString = "FormDeciderFormulaStringer: "
}
